package com.googlecode.kipler.container.dl;

import java.util.ArrayList;
import java.util.LinkedHashSet;
import java.util.List;
import java.util.Set;

import com.googlecode.kipler.container.dl.FormulaHolderDecider.Holder;
import com.googlecode.kipler.container.dl.creational.BoxFactory;
import com.googlecode.kipler.container.graph.RelationalValue;
import com.googlecode.kipler.satisfiability.reasoner.UnsatisfiableException;
import com.googlecode.kipler.syntax.formula.Formula;


/**
 * An implementation of possible worlds, that are used to explain the semantics
 * of modal logics, in the setting of this tableau algorithm.
 * 
 * @author İnanç Seylan
 * 
 */
public class World implements RelationalValue<World, String>, FormulaBase {
	/**
	 * The name of this possible world
	 */
	private String name = new String();

	private ABox aBox;

	private TBox tBox;

	private PBox pBox;

	private RBox rBox;

	private BoxFactory boxCreator;

	protected WorldConstraintSystem wcs;

	/**
	 * Default constructor
	 */
	public World(BoxFactory boxCreator) {
		this.boxCreator = boxCreator;
		createBoxes();
		aBox.setWorld(this);
	}

	/**
	 * Constructs a world with the given name.
	 * 
	 * @param name
	 *            The name of this world
	 */
	public World(BoxFactory boxCreator, String name) {
		this.boxCreator = boxCreator;
		createBoxes();
		aBox.setWorld(this);
		setName(name);
	}

	private void createBoxes() {
		aBox = boxCreator.createABox();
		pBox = boxCreator.createPBox();
		rBox = boxCreator.createRBox();
		tBox = boxCreator.createTBox();
	}

	/**
	 * @return the name of this world.
	 */
	public String getName() {
		return name;
	}

	public String getKey() {
		return name;
	}

	/**
	 * Sets the name of this world.
	 * 
	 * @param name
	 *            The name of this world
	 */
	public void setName(String name) {
		this.name = name;
	}

	public ABox getABox() {
		return aBox;
	}

	public TBox getTBox() {
		return tBox;
	}

	public PBox getPBox() {
		return pBox;
	}

	public RBox getRBox() {
		return rBox;
	}

	public WorldConstraintSystem getWcs() {
		return wcs;
	}

	public boolean isSatisfiable() {
		return aBox.isSatisfiable() && tBox.isSatisfiable()
				&& rBox.isSatisfiable() && pBox.isSatisfiable();
	}

	/**
	 * Adds the given formula to this world.
	 * 
	 * @param f
	 *            The formula to be added
	 * @return true if the formula is successfully added.
	 */
	public void addSilent(Formula f) {
		try {
			add(f);
		} catch (UnsatisfiableException e) {
		}
	}

	public void add(Formula f) throws UnsatisfiableException {
		Holder holder = FormulaHolderDecider.decide(f);
		switch (holder) {
		case ABOX:
			aBox.add(f);
			break;
		case TBOX:
			tBox.add(f);
			break;
		case RBOX:
			rBox.add(f);
			break;
		case PBOX:
			pBox.add(f);
			break;
		}
	}

	public boolean contains(Formula f) {
		Holder holder = FormulaHolderDecider.decide(f);
		boolean result = false;
		switch (holder) {
		case ABOX:
			result = aBox.contains(f);
			break;
		case TBOX:
			result = tBox.contains(f);
			break;
		case RBOX:
			result = rBox.contains(f);
			break;
		case PBOX:
			result = pBox.contains(f);
			break;
		}
		return result;
	}

	public Set<Formula> getFormulas() {
		Set<Formula> result = new LinkedHashSet<Formula>();
		result.addAll(getPBox().getFormulas());
		result.addAll(getTBox().getFormulas());
		result.addAll(getABox().getFormulas());
		result.addAll(getRBox().getFormulas());
		return result;
	}

	/**
	 * @see java.lang.Object#equals(java.lang.Object)
	 */
	@Override
	public boolean equals(Object obj) {
		if (obj != null && (obj.getClass().equals(this.getClass()))) {
			World other = (World) obj;
			// The conjunction rule must be applied to both of the worlds so
			// that their formulas are normalized. This takes care of situations
			// where one world contains a conjunctive formula and the other the
			// operands of that conjunctive formula.
			// TODO: do what's written above
			return getName().equals(other.getName()) && pBox.equals(other.pBox)
					&& aBox.equals(other.aBox) && tBox.equals(other.tBox)
					&& rBox.equals(other.rBox);
		}
		return false;
	}

	public World copy() {
		World world = new World(boxCreator, getName());
		world.pBox = pBox.copy();
		world.aBox = aBox.copy();
		world.aBox.setWorld(world);
		world.tBox = tBox.copy();
		world.rBox = rBox.copy();
		return world;
	}

	@Override
	public String toString() {
		StringBuffer buffer = new StringBuffer();
		buffer.append(getName());
		buffer.append(" = {\n");
		List<FormulaBase> fBases = new ArrayList<FormulaBase>();
		fBases.add(pBox);
		fBases.add(tBox);
		fBases.add(aBox);
		fBases.add(rBox);
		for (FormulaBase base : fBases) {
			buffer.append("   ");
			buffer.append(base);
			buffer.append("\n");
		}
		buffer.append("}");
		return buffer.toString();
	}
}
